Huet and Levy showed that index reduction is a normalizing strategy for every orthogonal strongly sequential term rewriting system. Toyama extended this result to root balanced joinable strongly sequential systems. In this paper, we present a class including all root balanced joinable strongly sequential systems and show that index reduction is normalizing for this class. We also propose a class of left-linear (possibly overlapping) NV-sequential systems having a normalizing strategy.

A computational model for security verification of cryptographic protocols is proposed. Until most recently, security verification of cryptographic protocols was left to the protocol designers' experience and heuristics. Though some formal verification methods have been proposed for this purpose, they are still insufficient for the verification of practical real-time cryptographic protocols. In this paper we propose a new formalism based on a term rewriting system approach that we have developed. In this model, what and when the saboteur can obtain is expressed by a first-order term of a special form, and time-related concepts such as the passage of time and the causality relation are specified by conditional term rewriting systems. By using our model, a cryptographic protocol which was shown to be secure by the BAN-logic is shown to be insecure.

Many rewriting systems, including those of terms, strings, graphs, and conjunction of atoms, are used throughout computer science and artificial intelligence. While the concepts of "substitutions," "places" in objects and the "replacement" of "subobjects" by other objects seems to be common to all rewriting systems, there does not exist a common foundation for such systems. At the present time, many of the theories are constructed independently, one for each kind of rewritten object. In the conventional approach, abstract rewriting systems are used to discuss common properties of all rewriting systems. However, they are too abstract to capture properties relating to substructures of objects. This paper aims to provide a first step towards a unified formalization of rewriting systems. The major problem in their formulation may be the formalization of the concept of "places". This has been solved here by employment of the concept of contexts rather than by formalization of places. Places determine subobjects from objects, while, conversely, contexts determine objects from subobjects. A class of rewriting systems, called β rewriting systems, is proposed. It is defined on axiomatically formulated base structures, called β structures, which are used to formalize the concepts of "contexts" and "replacement" common to many rewritten objects. The class of β rewriting systems includes very important systems such as semi-Thue systems and Petri Nets. Abstract rewriting systems are also a subclass of β rewriting systems.

This paper extends left-incompatible term rewriting systems defined by Toyama et al. It is also shown that the functional strategy is normalizing in the class, where the functional strategy is the reduction strategy that finds index by some rule selection method and top-down and left-to-right lazy pattern matching method.

Dynamic Term Rewriting Calculus is a new computation model proposed by the authors for the purpose of formal description and verification of algorithms treating Term Rewriting Systems. The computation of DTRC is basically term rewriting. The characteristic features of DTRC are dynamic change of rewriting rules during computation and hierarchical declaration of not only function symbols and variables but also rewriting rules. These features allow us to program metacomputation of TRSs in DTRC, that is , we can implement in DTRC in a natural way those algorithms which manipulate term rewriting systems as well as those procedures which verify such algorithms. In this paper, we give a formal description of DTRC. We then show some results on confluence property of DTRC.

The currying of term rewriting systems (TRSs) is a transformation of TRSs from a functional form to an applicative form. We have already introduced an order-sorted version of currying and proved that the compatibility and confluence of order-sorted TRSs were preserved by currying. In this paper, we focus on a key property of TRSs, completeness. We first show some proofs omitted in Ref. [3]. Then, we prove that the SN (strongly normalizing) property, which corresponds to termination of a program, is preserved by currying. Finally, we prove that the completeness of compatible order-sorted TRSs is preserved by currying.

This paper describes, from a system architectural viewpoint, how knowledge-based technologies have been utilized in developing EXLOG (an LSI circuit synthesis system) and SOFTEX (a software synthesis system) inside the authors' projects. Although the system architectures for EXLOG and SOFTEX started from the same production systems, consisting of transformation rules in the middle of the 1980's, both branched off in different directions in the 1990's. Based on experiences with EXLOG and SOFTEX, the differences between LSI and software design models are discussed, and the future directions are indicated for the knowledge-based design system architectures.

We extend the theorem of Gramlich on modular termination of term rewriting systems, by relaxing the disjointness condition and introducing the composability instead. More precisely, we prove that if R1, R-1 are composable, terminating term rewriting systems such that their union is nonterminating then for some a {1, -1}, Ra OR is nonterminating and R-aRa is Fa-lifting. Here, OR is defined to be the special system {or(x, y) x, or(x, y) y}, Fa is the set of function symbols associated with Ra, and an Fa-lifting system contains a rule which has either a variable or a symbol from Fa at the leftmost position of its right-hand side. The extended theorem is stronger than the original one in that it relaxed the disjointness and constructor-sharing conditions and allowed the two systems to share defined symbols in common under the restriction of composability. The corollaries of the theorem show several sufficient conditions for decomposability of termination, which are useful for proving termination of term rewriting systems defined by combination of several composable modules.

Dynamic Term Rewriting Calculus (DTRC) is a new computation model aiming at formal description and verification of algorithms treating Term Rewriting Systems (TRSs). In this paper, we show that we can use DTRC to mechanize explicit induction for proving an inductive theorem, that is, we can translate the statements of base and induction steps for proving by induction into a DTRC term. The translation reduces the proof of the statements into the evaluation of the corresponding DTRC term.

This paper presents a method for verifying safety property of a communication protocol modeled as two extended communicating finite-state machines with two unbounded FIFO channels connecting them. In this method, four types of atomic formulae specifying a condition on a machine and a condition on a sequence of messages in a channel are introduced. A human verifier describes a logical formula which expresses conditions expected to be satisfied by all reachable global states, and a verification system proves that the formula is indeed satisfied by such states (i.e. the formula is an invariant) by induction. If the invariant is never satisfied in any unsafe state, it can be concluded that the protocol it safe. To show the effectiveness of this method, a sample protocol extracted from the data transfer phase of the OSI session protocol was verified by using the verification system.

We propose a new type of Graph Rewriting Systems (GRS) that provide a theoretical foundation for using the reduction method which plays an important role on analyze network reliability. By introducing this GRS, several facts were obtained as follows: (1) We clarified the reduction methods of network reliability analysis in the theoretical framework of GRS. (2) In the framework of GRS, we clarified the significance of the completeness in the reduction methods. (3) A procedure of recognizing complete systems from only given rewriting rules was shown. Specially the procedure (3) is given by introducing a boundary graph (B-Graph). Finally an application of GRS to network reliability analysis is shown.